Inference at * 1 1 2 
Iof proof for Lemma connex iff trichot:



1. T : Type
2. R : TT
3. a, b:T. Dec(R(a,b))
4. x, y:T. R(x,y)  R(y,x)
5. a : T
6. b : T
7. R(b,a)
  (R(a,b) & (R(b,a)))  (R(a,b) & R(b,a))  (R(b,a) & (R(a,b))) 

latex

 by ((((Decide R(a,b)) 
CollapseTHENM (ProveProp))) 
CollapseTHENA ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	t  T, P & Q, P  Q, x(s1,s2), , Dec(P), x:A. B(x)
Lemmas	not wf